\begin{tabbing}
$M$.ef($k$,$x$,$s$,$v$,$w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(\=product{-}deq(Knd;Id;KindDeq;IdDeq);\+
\\[0ex](($M$.2.2.2.2).1);
\\[0ex]$<$$k$, $x$$>$;
\\[0ex]${\it kx}$,$E$.($w$ = $E$($s$,$v$) $\in$ $\mathbb{Q}\rightarrow$$M$.ds($x$)))
\-
\end{tabbing}